$\forall$$T$:Type. subtype\_rel($T$; $\mathbb{Z}$) $\Rightarrow$ ($\forall$$L$:($T$ List). sorted($L$) $\in$ prop\{i:l\})